R-compat{i:l}
R-compat(A; B)
== if Rplus?(A)
== ifthen R-compat{i:l}(Rplus-left(A); B)  R-compat{i:l}(Rplus-right(A); B)
== if Rplus?(B)
== ifthen R-compat{i:l}(A; Rplus-left(B))  R-compat{i:l}(A; Rplus-right(B))
== if Rnone?(A)
== ifthen True
== if Rnone?(B)
== ifthen True
== if eq_id(R-loc(A); R-loc(B))
== ifthen (fpf-compatible(Id; x.Type; id-deq; Rds(A); Rds(B))
== ifthen  fpf-compatible(Knd; x.Type; Kind-deq; Rda(A); Rda(B)))
== ifthen  if eq_bd(R-base-domain(A); R-base-domain(B))
== ifthen  then A = B
== ifthen  else R-frame-compat(A; B)  R-frame-compat(B; A)  R-discrete_compat(A; B)
== ifthen  fi 
== else R-interface-compat(A; B)  R-interface-compat(B; A)
== fi 

---

clarification:

R-compat{i:l}
R-compat(A; B)
== if Rplus?(A)
== ifthen R-compat{i:l}(Rplus-left(A); B)  R-compat{i:l}(Rplus-right(A); B)
== if Rplus?(B)
== ifthen R-compat{i:l}(A; Rplus-left(B))  R-compat{i:l}(A; Rplus-right(B))
== if Rnone?(A)
== ifthen True
== if Rnone?(B)
== ifthen True
== if eq_id(R-loc(A); R-loc(B))
== ifthen (fpf-compatible(Id; x.Type{i}; id-deq; Rds(A); Rds(B))
== ifthen  fpf-compatible(Knd; x.Type{i}; Kind-deq; Rda(A); Rda(B)))
== ifthen  if eq_bd(R-base-domain(A); R-base-domain(B))
== ifthen  then A = B  es_realizer{i:l}
== ifthen  else R-frame-compat(A; B)  R-frame-compat(B; A)  R-discrete_compat(A; B)
== ifthen  fi 
== else R-interface-compat(A; B)  R-interface-compat(B; A)
== fi 
(recursive) 

latex

Definitions	R-interface-compat(A; B), P  Q, R-discrete_compat(A; B), R-frame-compat(A; B), es_realizer{i:l}, s = t, R-base-domain(R), eq_bd(p; q), if b then t else f fi , Rda(R), Kind-deq, Type, Knd, fpf-compatible(A; a.B(a); eq; f; g), Rds(R), id-deq, Id, R-loc(R), eq_id(a; b), True, Rnone?(x1), Rplus-right(x1), f(a), Rplus-left(x1), Rplus?(x1), x.A(x), Y
FDL editor aliases	R-compat